GRACE TECHNICAL REPORTS
Bidirectional Transformation on Ordered Graphs
Fei Yang
Soichiro Hidaka
GRACE-TR 2015–08
December 2015
CENTER FOR GLOBAL RESEARCH IN
ADVANCED SOFTWARE SCIENCE AND ENGINEERING NATIONAL INSTITUTE OF INFORMATICS
2-1-2 HITOTSUBASHI, CHIYODA-KU, TOKYO, JAPAN
Fei Yang1and Soichiro Hidaka2
1 Eindhoven University of Technology, The Netherlands [email protected]
2 National Institute of Informatics, Japan [email protected]
Abstract. The linguistic (language-based) approach plays an important role in the development of well-behaved structural bidirectional transformations. It has been successfully applied to solve the challenging problem of bidirectional trans-formation on graphs by establishing a clear bidirectional semantics based on a bulk semantics of the structural recursion. However, this result was limited to un-ordered graphs, where the order between outgoing edges of nodes is disregarded, and it was not clear how to treat ordered ones such as XML documents with point-ers.λFGis a language for querying ordered graphs, in which, a bulk semantics of structural recursion, extended with children rearrangement capability, is provided in a unidirectional setting. In this paper, we show that (the first-order subset of) λFG can be bidirectionalized by a three-stage procedure. The forward evalua-tion generates a view graph with comprehensive order-aware trace informaevalua-tion. The traceable view enables us to reflect the edits on the view to the updates in the source by backward evaluation. We adopt a classical notion ofǫ-edges to represent the unobservable short cuts between nodes, which are fully utilized in bidirectionalization to keep the original shape of the input graphs. Thus our bidi-rectionalization is completed by a novel order-aware bidirectional procedure to eliminateǫ-edges.
1
Introduction
Bidirectional transformations [9,8] provide a graceful mechanism for the synchroniza-tion and maintenance of the structures and contents in transformasynchroniza-tions. They are perva-sive and have many potential applications, including the synchronization of replicated data in different formats [9], presentation-oriented structured document development, interactive user interface design [19], coupled software transformation, and the
well-knownview updatingmechanism which has been intensively studied in the database
community [3,10].
The linguistic (language-based) approach [9] gives us a promising way for the de-velopment of structured and well-behaved bidirectional transformation, in which ev-ery expression simultaneously specifies both a forward and the corresponding (correct) backward transformation, and every composition of expressions defines a structural glu-ing of smaller bidirectional transformations to a bigger one. Despite its usefulness for
bidirectional transformation on lists and trees [9,5,18,16,21], it is a challenge to imple-ment it on graphs. Firstly, unlike lists and trees, there is no unique way of representing, constructing, or decomposing a general graph, and this requires a more precise def-inition ofequivalencebetween two graphs. Secondly, graphs haveshared nodes and
cycles, which makes both forward and backward evaluation non-trivial; na¨ıve recursive
evaluation for tree structures would visit the same nodes possibly infinitely many times. In our previous work [14], we tackled the problem by showing that the linguistic approach can be applied to bidirectional transformation on graphs, where a clear bidi-rectional semantics is given for UnCAL, a graph algebra of the known graph query language UnQL [6]. The key to this success is that the bulk semantics of the structural recursion function is evaluated by first processing in parallelon all edges of the in-put graph and then combining the results. This bulk semantics relies onǫ-edges (short cuts between nodes like those in automata) to graphs, providing a smart way of treating shared nodes and cycles in graphs and of tracing back from the view to the source.
section
section
title
ref book
book
book book
section
“untyped λ-calculus” paragraph “introduction”
title refs
“data encoding” title “π-calculus”
book ref refs
section
title
“ λ-calculi” &
Fig. 1.Ordered Graph Representation of Books
However, the graphs that can be dealt with in this manner must be un-ordered, which means the order of out-going branches of nodes are disregarded. It has not yet been known, in a bidirec-tional setting, how to treat ordered graphs such as XML graphs like that in Figure 1 that represents book data with ordered sections and mutually cyclic references, where we would like to extract the dot-ted part to see outlines of the book, by selecting first sections (first branches are
rendered in thick arrows) while removing references, and further reflect the updates on the outline to the original book data. One might consider to encode the ordered graphs in terms of unordered ones by introducing some special edge labels, but this would make it difficult to keep consistency of the labels as discussed in [11]. In [11], a transforma-tion languageλFGfor ordered graphs is provided, where a bulk semantics to transform
ordered graphs is also given in unidirectional setting. Thus, a natural question is how we can bidirectionalize transformation on ordered graphs viaλFG. However, combination
of [11] and [14] is not straightforward, sinceλFGnot only respects the order of siblings
during transformation, but also rearranges them, like the example above that extracts only the first sections. The order-awareǫ-edge elimination should also be bidirectional-ized. It is required not only from user interface point of view where users usually do not directly operate on graphs withǫ-edges, but also from theoretical point of view because ǫ-edges should be eliminated before every structural recursion in ordered settings to make structural recursion well-defined [11].
In this paper, we show that the transformation on ordered graphs can be
bidirec-tionalized. An earlier attempt [12] with UnCALO also extended UnCAL. However,
UnCALO cannot rearrange siblings as we do in this paper. Our work is based on a
first-order subset ofλFG defined in [11]. As a result, we are able to bidirectionalize
men-tioned in this section. The first-order restriction comes from the fact that we do not have clear semantics of updates of function-type views. Nevertheless, we lose no expressive power relative to [14]. Rather, we have refined the condition in which well-behavedness is guaranteed in the presense of interference between variable bindings, as well as the strategies of edge-deletion reflections. The main technical contributions are three folds. First, a novel three-stage bidirectional transformation strategy is designed for ordered graphs. Next, we establish a bidirectional evaluation semantics forλFG. Finally, we give
an order-aware bidirectionalized procedure to eliminateǫ-edges.
Organization of the PaperWe shall start from a preliminary on the ordered graph model and the ordered graph transformation languageλFG in Section 2. In Section 3,
we present an overview of our three-stage bidirectionalization, and the properties which specify the goal of the design. The semantics of forward evaluation enriched with trace information, and backward evaluation to reflect view updates, are discussed in Sections 4 and 5. Then in Section 6, we present a bidirectionalized procedure for eliminating ǫ-edges. Finally, we discuss the related work and make a conclusion in Sections 7 and 8. The completed semantics, proofs and other materials are provided in the Appendix.
2
Preliminaries
2.1 Ordered Graphs
The Graph ModelWe start with an introduction of the formal definition for ordered graphs, which is inherited from [11].
We presuppose a finite setLoflabelsand an abbreviationLǫforL ∪ {ǫ}. LetXand
Y be finite sets of input and output markers, and we add the prefix&for markers like
&x. Anordered graph Gis defined by a triple (V,B,I), whereVis a finite set ofnodes,
B: V → List(Lǫ×V+Y) is the total function mapping a node to a list ofbranches:
a branch inLǫ ×V +Y is either alabeled edgeEdge(l,v) to nodevwith labell, or
anoutput markerOutm(&y), andI :X →Vis the total function which determines the
input nodes(roots) of the graph.
Example 1. The ordered graph in Figure 2(a), is represented as (V,B,I), where
V={1,2,3,4,5,6}
B={1→[Edge(ǫ,2),Edge(a,3),Edge(ǫ,4)],2→[Edge(ǫ,5)],3→[],
4→[Edge(a,3),Edge(b,6)],5→[Edge(a,6)],6→[Outm(&y)]} I(&)=1
We useGX
Y to denote a graphGwith an input marker setXand an output marker set
Y. Moreover, we writeGX
Y to represent the set of such graphs. Although the graph data
model in [11] also theoretically consider infiniteness of branches, it is sufficient for us to consider only finite cases.
For input markers, we allow a graph to have multiple roots. When the graph is single-rooted, we often use&as thedefault markerto indicate the root and useGY to
Proper Branches and BisimilarityIn the definition of ordered graphs,ǫ-edges are in-troduced to represent shortcuts between nodes. However, the sequence ofǫ-edges makes some observable branches of a node which are reachable from shortcuts implicit, i.e. we can not get every immediate observable branch of a node without searching through such sequence. We handle this difficulty by defining the notion ofproper branch, which is a path from a nodev, going through zero or moreǫ-edges until it reaches a non-ǫ -edge or an output marker. This notion relates the source and destination of an observable edge or an output marker.
Let us consider Figure 2(a) in which the list of branches of nodes are drawn in counter-clockwise order with the first branches marked by thicker lines. Node 1 and 6 are connected by two proper branches (1→−ǫ 2→−ǫ 5→−a 6 and 1→−ǫ 4→−b 6). However, such connectivity information does not appear explicitly in the branches before ǫ-elimination.
1 &
2 3 4
5 6 &y
1 &
2 3 4
5 6 &y
(a) (b)
a
a
b a
a
a a
b
a a
b a
Fig. 2.Two Equivalent Graphs
LetG=(V,B,I) andv∈V. The path starting fromv
v(=v0)→−ǫ i0v1. . . ǫ
−
→in−1vn→− in
(v→−l i denotes the i-th edge branch
(la-beled l) of node v) is called a proper
branchofvif thein-th branchB(vn).inis
not anǫ-edge (either a non-ǫedge or an output marker), and all the previous steps are ǫ-edges. The set of all proper branches ofvinGis denoted byPb(G,v).
We impose a total order on proper branches. Let us consider two proper branches in an arbitrary graph,p =(v→−ǫ i0v1. . .
ǫ
−
→in−1vn→− in), and p
′ =(v→−ǫ
i′
0v
′
1. . .
ǫ
−
→i′
n′ −1v
′
n′→− i′
n).
Let their branch index sequences be ˜p def= (i0, . . . ,in−1,in) and ˜p′ def
= (i′
0, . . . ,i
′
n′−1,i′n′).
We definep≤Pb p′
def
⇐⇒p˜ ≤l p˜′where≤lis the lexicographical order between branch
index sequences. This order helps us to define a bisimilarity andǫ-elimination as natural extensions of those in unordered setting, as well as to retain the correspondence of branches within the procedure of bidirectional elimination ofǫ-edges.
For a given proper branch p, we use p.lastto denote the last step of the branch sequence, which is either a non-ǫedge or an output marker.
2.2 The CoreλFG
λFG is a language for transforming (querying) ordered graphs. It is an extension of
typedλ-calculus with graph constructors and list functions. It has a powerful feature of structural recursion, and is capable of manipulating the sibling branches of nodes, which considerably extends the expressiveness of the language. The syntax ofλFG is
given as below, in which we only focus on a graph-related first-order subset.
e$x|λ$x.e e|(e,e)|prle|prre{terms of lambda calculus} |nil|cons(e,e)|foldr(e,e)|. . . {functions for lists} |ifetheneelsee|isEmpty(e) {conditional and emptiness}
|a|e=e {labels (a∈ L) and label equality}
|[]|ee|[e:e]|[&y]|&x≔e
|()|e⊕e|e@e|cycle(e) {graph constructors}
|srec(e,e)e {structural recursion functions}
prlandprrrespectively denote left and right projections of pairs.
The graph constructors are introduced in Appendix A, and the type rules are dis-cussed in Appendix B. The enriched semantics is briefly given in Section 4 and com-plemented in Appendix C.
Structural Recursion FunctionsHere we focus on the explanation ofstructural
re-cursion, which provides a mechanism to describe the queries and transformations that
guarantees termination of the computation and preserves finiteness.
In general a structural recursion is written as a function srec(e,d), where
e : Label×GY → GZZ is the body function applied on the labels of labelled edges and the subgraphs reachable from the edges, andd :List(GZ
Z×α+G Z
Z×Y) →G Z Z×α+Z×Y
is a rearrangement function manipulating sibling branches obtained from the body functions for each node. The output marker typeZ×αin the domain ofdcorresponds to the output marker branch produced by the body function, whereαis instantiated to node identifier and used to make connections to other fragment of the result
of structural recursion in the bulk semantics. Parametricity implied by α means
programmer ofd do not manipulate this output marker. Another output marker type
Z×Ycorresponds to the output marker branches of the input graph ofsrec. Therefore, the output markers in the result ofd are disjoint sum of these output marker types.
1
&
2 3 4
&y
1
& &y
4
&y
3 2
(a) (b)
a
b c
b a
b d
b d
Fig. 3.Source (a) and view (b) ofa2d xc
For an example of d, we consider a simple case whered=foldr(⊙, ι⊙) for some monoid
(⊙, ι⊙) onGZZ×α(graph type with sets of input
markers Z and output markers Z×α). We
provide a bulk semantics for the evaluation of structural recursion functions, and its trace-able forward semantics is given in Section 4.
Example 2. This example shows how to
ma-nipulate edges of the graph and change its shape by structural recursion. As shown in Figure 3, the following functiona2d xc replaces all labelsawithdand contracts
a2d xc=srec(rc,foldr( ˆ,[]))
where xˆ y =yx
rc($l,$g)=if $l=athen [d: [&]]
else if$l=cthen [&]
else [$l: [&]]
Example 3. The next example removes the branches in the even positions in the siblings
of the root. Thed funcitonprl◦(foldr(f,(nil,nil)))) is used to do the selection using
tupling technique [15].
even remove=srec(id,prl(foldr(f,(nil,nil))))
where id($l,$g)=[$l: $g]
f($x,$xs)=(prr$xs,cons($x,(prl$xs)))
Restrictions on the second argument ofsrec We restrict the form of the second
argu-mentdofsrecintofoldr(e1,e2), wheree1ande2should not necessarily form a monoid. Even with this restriction, the functiondcan do rearrangement (i.e., (1) swapping, (2) selection, (3) replication, (4) constructing new element) of siblings of given nodes by taking list of sibling graphs and returns another graph. Further graph transformations in (first-order subset of) λFG on these siblings are also possible. When e1 ande2 are restricted to monoids, selection of siblings like in Example 3 would not have been pos-sible.foldr, instead of unbiasedfoldon join list, is also crucial to achieve order-based selection like selecting the first element, in order to provide unique decomposition of sibling graphs.
Example 4. Figure 1 represents books with cyclic references. The following
transfor-mationoutlineextracts outlines of these books by selecting first sections while remov-ing references. The transformation returns the subgraph that is rendered with dotted edges.
outline=srec(λ($l,$g).[$l:fstsection(sections(cutref($g)))],foldr(,[]))
wherecutref =srec(λ($l,$g).if$l=refsthen[]else[$l: [&]],foldr(,[]))
sections =srec(λ($l,$g).if$l=sectionthen[$l: $g]else[],foldr(,[]))
fstsection=srec(λ($l,$g).[$l: $g],foldr(prl,[]))
d
1
2 3 4
b
b d
& & &
&
& & & &
& &
d
1
2 3 4
b
b d
(&,4) & &
&
(&,2) (&,3) & &
(&,4) (&,3)
d
1
2 3 4
b
b d
(&,&y)
(&,4) &
(&,2) (&,3)
(&,4) (&,3) (a)
(b) (c)
&
&y
&
(&,&y)
Fig. 4.Illustration of bulk semantics Bulk Semantics The
structural recursion of
λFG has two equivalent
semantics. One is
recur-sive semantics. It defines
the function behavior
and the program trans-formation/optimization recursively. It appears to be
Let us consider a structural recursionsrec(e,d). In the bulk semantics, the evalu-ation on every graph component is applied in parallel. It involves the following three steps (an enriched formal semantics is presented in Section 4). We shall also revisit the transformation a2d xcto transform the graph in Figure 3(a) to Figure 3(b). The corresponding bulk semantics is illustrated in Figure 4.
1. Map computation on edges withe: the functioneis applied on each labeled edge and the following subgraphs, yield a set of intermediate result graphs fore. These are surrounded by dotted round squares in Fig. 4(a). Results are bundled into list of graphs for each node of input graphs which are surrounded by dotted round squares in Fig. 4(b), where output markers are associated with the node id to be connected.
2. Map computation on nodes withd: The above list of graphs are merged by the
rearrangement measure defined ind, leading to a set of merged graphs for each node. In Figure 4(c), the rearrangement places the output marker branch under node 1 in the first position and edgedin the last position in the siblings.
3. Groups new graphs withǫ-edges: to get the final result, the graphs for each node need to be grouped together byǫ-edges. This is depicted in Figure 4(c). Theǫ-edges are added according to the input and output markers of the previous result. After ǫ-elimination, we the graph in Figure 3(b) is obtained.
3
An Overview of Bidirectional Transformation
3.1 Bidirectional Properties
GS GV
G′
V
G′
S
F[[e]]
update
B[[e]]
Fig. 5.Schema of Bidirectional Transformation
The bidirectionalization of transformation on ordered graphs is approached by pro-viding the bidirectional semantics ofλFG.
We aim to obtain a semantics that has bidirectional properties as defined in the previous work for UnCAL [14]. A whole picture of bidirectional transformation is shown in Figure 5. Let F[[e]]ρdenote a forward evaluation (get) of expression e
under environment ρ containing the source graph GS to produce a view GV, and
B[[e]](ρ,G′
V) denote a backward evaluation (put) of expressioneunder original
environ-mentρto reflect a possible modification on the viewG′
V to the source by computing an
updated environmentρ′, from which the updated source graphG′
S could be extracted.
An environmentρis a mapping with a form {$x → X, . . .}whereX is a graphGor
a labell, and $xis a variable. The transformation needs to satisfy the following two important properties (equality stands for exact equivalence here):
F[[e]]ρ=GV
B[[e]](ρ,GV)=ρ (GETPUT)
B[[e]](ρ,G′
V)=ρ
′F[[e]]ρ′=G′′
V
B[[e]](ρ,G′′
V)=ρ
′ (WPUTGET)
The (GETPUT) property states that unchanged viewGV should give no change on
the environmentρin the backward evaluation, while the (WPUTGET) property states that the modified viewG′
V and the viewG
′′
V obtained by backward evaluation onG
′
V
same effectρ′on the original sourceρif backward evaluations are applied on them. We consider a pair of forward and backward evaluation iswell-behavedif it satisfies
(GETPUT) and (WPUTGET) properties.
In general, forward and backward transformations may not be totally defined. In our language, forward transformation fails ifǫ-elimination fails, and we have an effective decision procedure [11]. Backward transformation fails if the update on the view is not propagable, like update of constant values created in the transformation. See Sections 4 and 5 for more detail on each case of failure.
On our proposed bidirectionalization, we have the following theorem.
Theorem 1 (Well-behavedness).The proposed forward and backward evaluations on
λFGare well-behaved, provided their evaluations succeed.
According to the (WPUTGET) property, given a certain forward evaluation func-tion, there could be more than one backward evaluation that would satisfy the well-behavedness property. Moreover, the modifications on the view graph could be catego-rized into three types: in-place updates (edge-renaming), edge deletion and subgraph insertion. We select the rational choice for updating the source graph by three princi-ples:location correspondenceto reflect modifications on the corresponding part in the source, theleast change[19] on the set of updating edges, and themonotonicityon the modification operations (deletion is reflected to deletion, and so on). Henceforth, such choice could be a prescriptive goal in designing the bidirectional transformation. The goal is to let the updates on the source most possibly meet the intention of the users for the change on the view.
3.2 Three-Stage Bidirectionalization
In UnCAL, a two-stage framework is proposed for bidirectionalizing unordered graph transformation [14], in which during the forward transformation we first apply the eval-uation with semantics enriched with trace information, then eliminate theǫ-edges to produce a usual view.
The most challenging part of bidirectionalization onλFGcomes from the capability
of rearrangement of sibling branches in the structural recursion. It requires a three step bulk semantics as discussed in Section 2, which makes it more complicated to retain a consistent trace between the source and view. The original method in [14] is not capable of handling the sibling transformations. Further, there is a requirement that the structural recursion with generald function only accepts input graphs withoutǫ-edges to keep the bisimulation genericity (actually, the presence ofǫ-edges breaks the bisimulation genericity, see [11] for a counterexample). Thus, anǫ-elimination procedure is essential before applying the structural recursion for an arbitrary graph. Also, theǫ-edge should be eliminated before it is presented to the end-user. Moreover, the order of the branches must be recorded during the bidirectional transformation. Our basic idea is to divide the forward evaluation into three stages, each of which could be bidirectionalized.
– Stage 2: Forward evaluation using bulk semantics. This stage may create some newǫ-edges, so that the output graph will have a similar shape to the input graph. Appropriate trace information might be appended locally on the nodes in the result graph.
– Stage 3: Elimination ofǫ-edges to produce a usual view. The method is the same as that in Stage 1.
In our bidirectional transformation framework, we will propose in Section 6 a gen-eral bidirectionalizedǫ-edge elimination procedure for both Stage 1 and Stage 3. For Stage 2, a bidirectionalized semantics forλFG is provided in Section 4 and 5. Thus, the
whole transformation is bidirectionalized by an inductively defined procedure.
4
Traceable View and Reflection of Inplace-Updates
Practically, a λFG expression usually specifies a forward transformation that maps a
source ordered graph (possibly a database or an XML file) to a view graph, and a back-ward transformation is the procedure to reflect view updates to the source graph. How-ever, the structural information kept byǫ-edges is implicit in the view graph. Moreover, the newly constructed parts during transformation can not be traced back in the source. In this sense, some appropriate trace information (like provenance traces [7]) should be added to the view, to make the view more informative, in other words,traceable. In this section, we will enrich the original semantics ofλFG to produce a traceable view after
forward transformation.
4.1 Local Trace Information
In our scenario, a view is obtained by evaluating a λFG expression with an ordered
graph. A node in the view graph could be obtained from the source graph, or con-structed by theλFG expression, or generated by a structural recursion function (in bulk
semantics). To record this lineage of computations, we wrap the tracing information up in every node locally in the view graph. We defineTraceIDfor every node as
TraceID≔SrcID |CodePos Marker
| RecNPos TraceID Marker |RecEPos TraceID TraceID Num
| RecMPos Marker TraceID Num|RecD Pos TraceID TraceID
whereSrcID ranges over the identifiers uniquely assigned to all nodes in the source graph,Posranges over code positions in theλFG expressions,Markerranges over
in-put/output makers, andNumranges over the lists of integers, which represent the posi-tion of the branch among its siblings.
Now we briefly explain the information recorded by eachTraceID.SrcIDmeans the node is generated from the corresponding one in the source.Code p&mis the informa-tion for the nodes created by theλFG constructor on the code position p, where&m
is used only for constructors involving markers.RecN,RecE,RecM,RecDare four kinds of trace information used in bidirectionalizing structural recursionsrec(e1,d)(e2).
which are generated from the nodes/non-marker branches/output marker branches re-spectively, andRecDinformation is added when the rearrangements on the lists of sib-lings are applied byd. RecN p v&mdenotes a node originated from nodevgenerated bye2for component&m(each component of mutually recursive functions are encoded by a marker), and it corresponds to nodes1 through4 in Figure 4.RecE p v w i de-notes a node originated from nodewgenerated bye1, which in turn is generated byi-th branch of nodevgenerated bye2, and nodewcorresponds to the nodes drawn with small circles in the round dotted squares except the one on the right bottom of Figure 4(a).
RecM p&m v idenotes a node originated fromi-th marker (&m) branch of nodev gener-ated bye2, and corresponds to the nodes drawn with small circles in the dotted squares on the right bottom of Figure 4(a). andRecD p v w denotes a node originated from nodevgenerated by the functiondapplied on nodew, where the nodew(∈TraceID) is marked byRecNand identifies the list appeared in thatdfunction. RecDconstructor is applied to the nodes drawn with small circles in Figure 4(b) and (c).
4.2 Enriched Bidirectional Semantics and the Reflection of Inplace-updates
Now we proceed to define the enriched forward semantics of λFG which generates a
traceable view. Compared with the original semantics [11] ofλFG, the trace
informa-tion is recorded whenever a node is created by the forward transformainforma-tion. For each expression, we define its backward evaluation reflecting the inplace-update. We adopt the notion of code position to specify the expression which creates new graph elements. Letep denote aλ
FG subexpressioneat code position p. We write ρ($x) forG when
($x → G) ∈ ρ, andeρapplies the variable substitution usingρin the expressione. We only give the semantics for some representative expressions here, and complete with the remaining operators in Appendix C D. Moreover, the well-behavedness of the semantics is discussed in Appendix F
In order to merge the updated environment computed by the backward evaluation, we introduce a merge operator [14].
ρ1⊎ρρ2=
(x→mg(G,G1,G2)
(x→G1)∈ρ1 (x→G)∈ρ (x→G2)∈ρ2
wheremg(G,G1,G2)=
G1 ifG2=G∨G1 =G2
G2 ifG1=G
FAILotherwise
The operator⊎ρ unifies environments on both hand sides (ρ1 andρ2) updated relative to original environmentρ. For each variablex, if only one binding is updated, or both bindings are updated consistently, then the updated binding is adopted. Otherwise, the unification of inconsistent updates fails.
Graph Constructor ExpressionsThe functions of graph constructor expressions are illustrated in Appendix A. For instance, the enriched forward semantics of single node graph constructor at code positionpis (see also Figure 6(a)),
F[[[]p]]ρ=({Code p},{Code p→[]},{
&→Code p}).
Code p
&
F[[[]p]]ρ F
[[(e1e2)p]]ρ
Code p&x1 &x1
Code p&xm &xm
F[[e1]]ρ F[[e2]]ρ
. . .
. . .
(a) (b)
Fig. 6.F[[[]p]]ρandF[[(e
1e2)p]]ρ
As its forward evaluation only generates a constant graph, in the backward evalua-tion, no modification is accepted on the view. The backward semantics is defined as:
B[[[]p]](ρ,G′)=ρ if G′=F[[[]p]]ρ FAILotherwise
Here, the parameterρis the original environment andG′is the updated view. We simply require thatG′is equal to the result of forward evaluation onρ. Thus the well-behavedness property is guaranteed whenever the backward evaluation succeeds.
For another example, the enriched forward semantics of the expressione1e2 is defined as follows (see also Figure 6(b)).
F[[(e1e2)p]]ρ=F[[e1]]ρpF[[e2]]ρ
where G1pG2 =(V1∪V2∪V′,B1∪B2∪B′,I′) (V1,B1,I1)=G1
(V2,B2,I2)=G2
M =inMarker(G1)=inMarker(G2)
V′ ={Code p&m|&m∈M}
B′ ={Code p&m→[Edge(ǫ,I1(&m)),Edge(ǫ,I2(&m))]|&m∈M}
I′ ={&m→Code p&m|&m∈M}
where p is a union operator for two graphs concerning position p. We write
inMarker(G) andoutMarker(G) to denote the set of input and output markers in a graphG, respectively.
For its backward evaluation, we first decompose the updated graphG′ and ap-ply backward transformation on each of the subexpressionse1ande2 using the frag-ment graphs. We have the following definition, givendecompG1G2(G
′) defined in
Ap-pendix D as the decomposition of the graphG′, then B[[(e1e2)p]](ρ,G′)=B[[e1]](ρ,G′1)⊎ρB[[e2]](ρ,G′2)
whereG1=F[[e1]]ρ, G2=F[[e2]]ρ (G′1,G′2)=decompG1pG2(G
′)
VariablesThe query of ordered graph viaλFGrequires lambda abstraction and variable
reference. The forward semantics for variable reference looks up the variable in the environmentρand returns its binding.
For an inplace-update, a variable simply updates its bindings asB[[$v]](ρ,G′) =
ρ[$v←G′]. Here,ρ[$v←G′] is an abbreviation for (ρ\ {$v→ })∪ {$v→G′}.
ConditionThe forward semantics of a condition is defined as
F[[(ife1thene2elsee3)p]]ρ=
F[[e2]]ρifF[[e1]]ρ
F[[e3]]ρotherwise
It first evaluates the conditional expressione1, and it chooses the right branch to evaluate according to the result of the conditional expression.
And the procedure of its backward evaluation is defined by
B
ife1thene2
elsee3
(ρ,G′)=
ρ′2 ifF[[e1]]ρ∧F[[e1]]ρ′′
2,whereρ
′
2=B[[e2]](ρ,G
′)
ρ′′
2 =pr(ρ
′
2,utrans(upd∆,t′1))
t′
1 =external trace fore1(see Section F) ρ′
3 if¬F[[e1]]ρ∧ ¬F[[e1]]ρ
′′
3,whereρ
′
3=B[[e3]](ρ,G
′)
ρ′′
3 =pr(ρ
′
3,utrans(upd∆,t′2))
t′
2 =external trace fore2
FAILotherwise
It is reduced to the backward evaluation ofe2ife1holds, and to the backward evaluation ofe3 otherwise. To guarantee well-behavedness, we further ensure that the boolean expressione1does not change after backward evaluation. Because the result ofe1may be influenced indirectly by backward evaluation of the bodiese2 ande3, if they update variable bindings, and the values of variables in the condition are produced from the updated bindings. It is essential to check the value of the condition with the new binding of variables. To compute the influence, we separately compute, for every expression, the mapping from every edge produced by the expression, to the corresponding edge in the source graph (if the view edge is originated from the edge in the source graph), and use these mappings to reflect (top-level) view updates to the edges bound to free variables ine1. It is achieved by a mechanism similar to the classification of view edges used in [13]. See equation BIfin Appendix F for the detailed description.
1 GE1,(1) GE1,(2) GE1,(3)
2 GE2,(1)
3 GE3,(1)
4 GM4,(1)
RecE1 1 (1)
&m
RecE2 1 (1)
(&m,RecN2)
RecM&y4 (1)
&m
(&m,y)
RecN1
(&m,&y)
RecN4 RecN3 RecN2
GE1,(2) GE1,(1)
GE2,(1)
GE3,(1)
GM4,(1) GE1,(3) (a)
(b)
(c) (d)
d
Fig. 7.Forward Evaluation of Bulk Semantics Structural RecursionFigure 7
illustrates an overview of bidi-rectionalization of structural re-cursion functions. It applies the transformation in Example 2 to the source graph in Figure 3(a) to get a view graph in Fig-ure 3(b). For simplicity, we omit code positions in these figures. As shown in Figure 7(a), the forward evaluation first applies edge mapping using body ex-pressionebwhich isrc, and re-sults in a mapping from every node to a list of subgraphs. Two
and merging with ǫ-edges are illustrated in Figure 7(d). Finally, the view graph in Figure 3(b) is obtained by anǫ-elimination procedure.
An overview of the forward evaluation is given below. Note that the functions
EMap, DMap and Merge are defined for edge mappingeb, list mappingd and view
construction respectively. F[[(srecZ(eb,d)(ea))p]]
ρ =(g′)
whereg′ =Merge(g.V,BDMap,g.I) g=F[[ea]]ρ
EMap(B) ={u→BMap(x)|(u→x)∈B}
BMap(x) =
ELable(F[[eb]]ρ′,v,u,i) b=Edge(l,v)
ρ′=ρ∪ {$l→l, $g→g|v}
(MLabel(&y,u,i)) b=Outm(&y)
(b,i)∈L x
DMap(B)={u→(λg.DLabel(g,u))F[[d]]ρ∪{$b→x}|(u→x)∈B}
BDMap =DMap(EMap(g.B))
[e|(x,i)∈L l]def= [e|x=l.i]i∈|l|
Backward evaluation of a structural recursion function is defined by the fol-lowing stepwise procedure. It performs an inverse procedure of the forward evaluation. The most crucial point is to decompose the updated view graphs
and to remove the ǫ-edges generated during the forward evaluation using trace
information. Further, when we merge the updated environment, we first merge local updates on environments of body expressions, and then merge them to the whole updated environment. Since there might be overlapped parts among them, we let the backward evaluation fail if the overlapped parts are inconsistent.
B[[srec(eb,d)(ea)]](ρ,G′
srec)=B[[ea]](ρ,G′)⊎ρ{ρ′v,i\ {$l→ } \ {$g→ }}
where (Vsrc,Bsrc,Isrc)=F[[ea]]ρ, (Vsrec′ ,B′srec,I′srec)=G′srec
G′=(V′∪ρ′
v,i($g).V,B
′∪ρ′
v,i($g).B,Isrc)
V′={v|(v→ s)∈B′} ∪ {w|Edge(l,w)∈s,(v→ s)∈B′}
B′=EMap′(B′
EMap)=EMap
′(DMap′(Merge′(G′
srec)))
Merge′(G′)={u→(VMerge′(G′.V,u),BMerge′(G′.B,u),IMerge′(G′.B,u))|u∈V
src} DMap′(B′
DMap)={u→B[[d]](ρu,DLabel
′(B′
Dmap(u)))($b)|u∈V} EMap′(B′
EMap)={u→
emapB′(u,b,i)|(b,i)∈
L x|(u→x)∈B′EMap}
emapB′(u,b,i)=
Edge(ρ′
u,i($l), ρ
′
u,i($g).I(&))
whereρ′u,i=B[[eb]](ρu,i,ELabel′(G
u,i))
(b,i)=(GEu,i,i)
MLabel′(G
Mu,i) (b,i)=(GMu,i,i)
We put the complete semantics for the bidirectional transformation of structural re-cursion functions in Appendix CD, where the detailed explanation of every subfunction can be found.
5
Reflection to Deletion and Insertion
updates: (1) edge-renaming (in-place updates), (2) edge-deletion, and (3) insertion of edges or a subgraph rooted at a node. We already have dealt with the first case in Sec-tion 4. In this secSec-tion, we proceed to reflect the other two types of updates.
5.1 Reflection of Edge Deletion
Similarly to the method in our previous work in [14], we reflect deletion of an edge in the view as deletion of corresponding edge in the source utilizing the information withinTraceIDs. Here we identify an edge in the view by a tuple of its origin node and branch order.
The functioncorrdefined below computes a corresponding edge of an edge in the view as a tuple of origin node ID and its branch order in the source.
corr((u,i))=(u,i) ifu∈SrcID corr((RecE p u v i,j))= corr((u,j))ifcorr((u,j))FAIL
corr((v,i))ifcorr((u,j))=FAIL
corr((RecD p u v,j))=corr((u,j)) corr(ζ)=FAIL otherwise
FAILmeans failure in finding the corresponding edge. Also note that for theRecE -labeled branches, we choose the corresponding edge from the body expression of struc-tural recursion first, rather than from the argument expression, to make the change to the new view created by the next forward transformation smaller (we later discuss as the principle of least change [19]). When the tracing hits the edge created by the query
(theTraceIDmust be of the formCode), the evaluation fails. Moreover, the user would
be informed of such invalid deletion.
Note that only non-ǫedges are allowed to be deleted in the view. Thus, a node with trace informationRecNorRecMnever appears as an argument ofcorr.
Suppose the user deletes one edge, say (u,i) on the view graphGV. We can get
one corresponding edge on the sourcecorr((u,i)). In fact, multiple edges from the view
GV might have the same value on corrwith (u,i). LetDu,i = {(v,j) | corr((v,j)) =
corr((u,i))}. The set is computed by an enumeration on all the edges inGV. We adopt
G′
V =GV −Du,ias the updated view.
The failure of the computationcorr((u,i)) results in the failure of backward evalua-tion. Otherwise, we compute the updated sourceG′
S by removal ofcorr((u,i)) inGS. As
mentioned in Section 2.1, we use a list of integers as the branch order, which forms a total order. Thus the relative position of the following (sibling) branches will not change if we delete one edge.
Finally, we returnρ′=ρ[$g→G′
S], ifF[[e]]ρ
′=G′
V, or failure otherwise. One of
the cases of failure here is that, the deletion ofcorr((u,i)) inGS changes the value of
boolean expressions during evaluation of some condition clauses. It would change the evaluation into the other branch in such condition clauses, which is invalid according to our assumption that the value of boolean expressions are invariant during the view up-dates.
srec((λ($l,$g).
if $l=athen srec((λ($l,$g).
if $l=bthen$db
else[]),id)($db)
else[]),id)($db) Another case of the violation of (WPUTGET)
can be demonstrated as follows. For the query on the right, suppose we have graph [a,b,c] and removeaon the view. Then we trace back the edgeaand deleteaon the source.
transfor-mation on that empty view will result in an empty source graph. Therefore, ( WPUT-GET) is not satisfied. The checking rules out these cases. For the successful case, a querysrec((λ($l,$g).if $l=athen$gelse[]),id)($db) with the same input graph will extract subgraph under edge labeleda, i.e., [b,c]. Then the deletion ofcsucceeds. The trace-based approach is unable to detect the change of reachability or boolean values caused by edge deletion. Nevertheless, such failures are distinguished from invalid up-dates on the query (which could be detected by thecorrfunction). A compromise to detect such failures is to use a final check to conclude the failure of evaluation.
Hence, the (WPUTGET) property is straightforward (actually we are imposing
stronger (PUTGET) property) from our final check, which leads to the
well-behavedness. A natural question is to avoid the final check and the failure of evaluation. To do so, we provide an alternative solution with more refined semantics as well as a more detailed case study on the user’s intention of updates in Appendix E.
5.2 Reflection of Subgraph Insertion
The method used in previous work of handling insertion in unordered graph [14] can be adopted here.
The insertion operation on the view is specified by a triple of a nodevon the view and the positioniwhere a graph is inserted, and the inserted graphGvins. Then we first compute the corresponding source nodeuat which insertion of corresponding subgraph
Gsinstakes place, by the following functiontr.
tr(SrcID)=SrcID tr(RecN v )=tr(v) tr(Code )=FAIL
tr(RecE v )=tr(v) tr(RecD v )=tr(v) tr(RecM )=FAIL
We find a graphGsinsconnected touand the corresponding positionjat whichGsins is connected, by inversion computation onG′
Vusing the Universal Resolving Algorithm
(URA) [1], whereG′
Vis obtained by addingǫ-edge fromvat positionitoGvins. Further,
we conjecture that well-behavedness of the above insertion reflection can be directly derived from the soundness of URA.
6
Bidirectionalizing
ǫ
-Elimination Procedure
The idea of the ǫ-elimination procedure is to substitute the shortcuts within proper branches with new labeled edges. As mentioned in Section 2.1, we use a list of inte-gers as a total order over proper branches on a node, so we are able to access one of the branches from the list by a list of integers (denoted ˜pbelow) rather than a single integer. For a graphG = (V,B,I) ∈ GXY, theǫ-eliminationǫ-elim(G) ofG gets a graph
(V,B′,I) ∈ GX
Y. We let |B
′(v)| def= |Pb(G,v)|, and B′(v).p˜ def= Pb(G,v).p˜.last, where
Pb(G,v).p˜ is a proper branchp =(v→−ǫ i0. . .vn→− in) in B
′(v). Note that this procedure
could fail. Since if there are someǫ-edge cycles, it would lead to infinite number of proper branches, as mentioned in [11]. We use the effective procedure in [11] to decide the eliminability ofǫ-edges.
Next we will introduce a mechanism to reflect view updates overGV =ǫ-elim(GS)
to the source graph GS. We make use of the correspondence between the proper
1. For the in-place updates on an arbitrary edge B′(v).p˜ ∈ GV, the corresponding
labeled edge on the source isPb(GS,v).p˜.last. We just apply the same in-place
update operation on this edge.
2. For the deletion of an edgeB′(v).p˜ ∈GV, we update the source graph by deleting
the corresponding edgePb(GS,v).p˜.last.
3. For the edge insertion, since the set of nodesV is the same on the view and the source, we just need to insert the edge to the same location on the source.
After we have done the update operation on the source, anǫ-elimination procedure need to be applied again on the updated source. The reason is that, the updated labeled edge may be duplicated in different branches in the view. For example, in Figure 2, (b) is the graph obtained byǫ-elim from (a). Thea-labeled edge from nodes 5 to 6 in (a) is related with threea-labeled edges, respectively from node 1,2 and 5 to node 6 in (b). In case one of them is deleted, we need to delete the rest to retain the consistency. Thus, the corresponding edges of these proper branches on the view graph need to be updated to maintain the consistency between the source and the view. Therefore, the whole procedure would satisfy the well-behavedness. Moreover, three principles for rational updates in Section 3.1 are also implied from this constructive bidirectionalizing procedure.
7
Related Work
In the database community, bidirectional transformation has been discussed as view updating problem. Bancilhon and Spyratos proposed a general approach to this problem in [3]. The method was to define a constant complement view, from which the original database can be computed with the correlated information in the user-defined view. This method was applied to relational databases [10,17], as well as tree structures [18]. The constant complement view satisfies a very strong bidirectional properties at the sacrifice of the number of reflectable updates. It was too strong for our purpose, i.e., model transformation in software engineering, despite some particular applications [10]. A lot of linguistic approaches in the area of programming languages was proposed [8,9,5] for strings, trees and relational databases. However, they are difficult to be applied on graphs models due to the cycles and sharing nodes in graphs. In the context of software engineering, there has been several works on bidirectional (graph) transformation, one of the representative methods is the triple graphs grammars [20], which is powerful in graph transformation, however still not implemented on ordered graphs.
order function [11], while keeping all the UnCAL features. The present work joins3the above two research lines – bidirectionalization from [14] and order introduction from [11]. However, this is not just a simple combination. In [14], we reused the Skolem terms in the bulk semantics for trace information to decompose target graphs, and two-stage bidirectionalization enabled to defer all theεelimination at the end of the entire forward transformation. However, when sibling transformation is introduced in [11], to keep the structural recursion well-defined,εhave to be eliminated for every structural recursion application, which means we can no longer use two-stage bidirectionalization strategy. Therefore our bidirectionalεelimination is inserted along with every structural recursion application. Also, [14] did not discuss the diversity in the backward transfor-mation reflection strategy as we did with respect to least-change principles [19], in particular, in the edge-deletion handling. Moreover, [14] did not have clear condition to keep WPutGet property in relation to branching behavior change, while we clarified using the classification of edges similarly to that in [13]. With respect to [11], higher or-der transformation was dropped, because we do not have clear semantics of the updates on functional values. We lose no expressive power relative to[14].
With respect to the notion of traces, apart from general studies like provenance traces [7], self-adjusting computation by Acar et al. [2] also leaves traces during com-putation, to make the recomputation with slightly modified input efficient, utilizing the locality of the modification. Dynamic dependency graph is used to record the depen-dencies among data and computations. In the present paper, we also leave trace dur-ing forward computation. Although our trace IDs are natural extensions of the Skolem functions, we could also consider them as run-time relation between operations and data, because we associate the code position of the operators with the edges and nodes in the arguments of the Skolem functions. However, we propagate the changes in the opposite direction, from output to input. Therefore we would not be able to reuse the same technique, at least in a direct manner. However, as we mention in the conclusion, with pure trace approach, we could have propagated changes directly through mapping between source and target edges, with branching behavior change checking. Then our approach would become closer to the self-adjusting computation approach in the sense that trace is used to exploit locality. Instead, we currently reverse all the computation regardless of the presence of the modification.
Handling ordered structure in the bidirectional transformation has been studied ex-tensively through lenses [9], later improved to deal with rearranging updates through dictionary lenses [5] with key-based alignments, and the alignment strategies were gen-eralized through matching lenses [4]. Although we support rearranging by the trans-formation, our update is operation based, so update should always be decomposed into edge renaming, edge deletion and subgraph insertion. Rearranging update cannot be fed to our backward transformation directly.
8
Conclusion
In this paper, we bidirectionalized transformation on ordered graphs, in which a three-stage bidirectionalizing strategy is provided. With trace-enriched semantics, we are able to reflect three kinds of view updates: inplace updates, edge deletion and subgraph insertion. In future work, we plan a practical implementation. Also, we would like to utilize the externalized traces defined in Appendix F that directly maps between source and target edges/nodes for reflecting other than inplace updates.
Acknowledgement.We thank the authors of the paper [12] on which our present work is built. We also thank Prof. Zhenjiang Hu for his valuable comments and suggestions.
References
1. S. M. Abramov and R. Gl¨uck. Principles of inverse computation and the universal resolving algorithm. InThe Essence of Computation, pages 269–295, 2002.
2. U. A. Acar, G. E. Blelloch, and R. Harper. Adaptive functional programming. ACM Trans. Program. Lang. Syst., 28(6):990–1034, Nov. 2006.
3. F. Bancilhon and N. Spyratos. Update semantics of relational views. ACM Transactions on Database Systems (TODS), 6(4):557–575, 1981.
4. D. M. J. Barbosa, J. Cretin, N. Foster, M. Greenberg, and B. C. Pierce. Matching lenses: Alignment and view update. InICFP’10, pages 193–204. ACM, 2010.
5. A. Bohannon, J. N. Foster, B. C. Pierce, A. Pilkiewicz, and A. Schmitt. Boomerang: Re-sourceful lenses for string data. InPOPL ’08, pages 407–419, 2008.
6. P. Buneman, M. Fernandez, and D. Suciu. Unql: a query language and algebra for semistruc-tured data based on structural recursion.The VLDB Journal, 9(1):76–110, 2000.
7. J. Cheney, U. A. Acar, and A. Ahmed. Provenance traces.CoRR, abs/0812.0564, 2008. 8. K. Czarnecki, J. N. Foster, Z. Hu, R. L¨ammel, A. Sch¨urr, and J. F. Terwilliger. Bidirectional
transformations: A cross-discipline perspective. InICMT’09, pages 260–283, 2009. 9. J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, and A. Schmitt. Combinators for
bi-directional tree transformations: A linguistic approach to the view update problem. ACM Transactions on Programming Languages and Systems (TOPLAS), 29(3):17, 2007. 10. S. J. Hegner. Foundations of canonical update support for closed database views. In
ICDT’90, pages 422–436. Springer, 1990.
11. S. Hidaka, K. Asada, Z. Hu, H. Kato, and K. Nakano. Structural recursion for querying ordered graphs. InICFP’13, pages 305–318, Sept. 2013.
12. S. Hidaka, K. Asada, H. Kato, K. Nakano, and Z. Hu. Towards bidirectional transformations on ordered graphs. National Institute of Informatics, GRACE-TR-2011-07, Dec. 2011. 13. S. Hidaka, M. Billes, Q. M. Tran, and K. Matsuda. Trace-based approach to
editabil-ity and correspondence analysis for bidirectional graph tansformations. Technical report, May 2015. http://www.prg.nii.ac.jp/projects/gtcontrib/cmpbx/tesem.pdf, extended summary appears in proc. of BX 2015.
14. S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graph transformations. InICFP’10, pages 205–216, 2010.
17. J. Lechtenb¨orger and G. Vossen. On the computation of relational view complements.ACM Transactions on Database Systems (TODS), 28(2):175–208, 2003.
18. K. Matsuda, Z. Hu, K. Nakano, M. Hamana, and M. Takeichi. Bidirectionalization trans-formation based on automatic derivation of view complement functions. InICFP’07, pages 47–58, 2007.
19. L. Meertens. Designing Constraint Maintainers for User Interaction. http://www.kestrel.edu/home/people/meertens/, 1998.
20. A. Sch¨urr and F. Klar. 15 years of triple graph grammars. InICGT ’08: Proceedings of the 4th international conference on Graph Transformations, pages 411–425. Springer-Verlag, 2008.
A
Graph Constructors
[] [a : G]
G a
G &x := G
&x
()
&x1 ... &xk
&y1 ... &yn
&x’1 ... &x’m
&y1 ... &yn
G1 G2
G1G2 G1@G2
&x1 ... &xk
&y1 ... &ym
G1
&z1 ... &zn
&y1 ... &ym
G2 ε ε
cycle(G)
&x1 ... &xm
&x1 ... &xm ε ε
G [&y]
&y
G1 ++ G2
G1 G2 &x1 ... &xm
&y1 ... &yn
Fig. 8.Graph Constructors
We have nine graph constructors (Figure 8) as the operators to construct ordered graphs inductively.
G[] {single node graph}
| G1G2 {graph concatenation}
| [a:G] {an edge pointing to a graph} | [&y] {a node graph with
output marker}
| &x≔G {label the root node with an input marker}
| () {empty graph}
| G1⊕G2 {disjoint graph union}
| G1@G2{append of two graphs}
| cycle(G) {graph with cycles}
The single node graph constructor [] constructs a root-only graph.G1G2 joins two graphs by connecting every pair of roots fromG1 andG2to a new root withǫ-edges. [a :G] adds analabeled edge pointing to the root ofG. [&y] constructs a single node graph with an output marker&y.&x≔Gassociates an input marker&xto the root node ofG. () constructs an empty graph with neither a node nor an edge.G1⊕G2joins two graphs by using a componentwise (V,B,I) union. Note thatunifies input nodes while
⊕does not.G1@G2joins two graphs by connecting the output marker branches ofG1 with the corresponding input nodes ofG2withǫedges.cycle(G) connects the output marker branches ofGwith the corresponding input nodes withǫedges, which would form cycles.
For the set of input nodes of constructed graphs, the set of input markers ofG1and
Whereas the set of input markers ofG1andG2inG1⊕G2are disjoint, and their union becomes the new set of input markers. ForG1@G2, the input nodes of the first operand becomes the new input nodes and the input nodes of the second operands are connected with the output marker branches if exists.
B
Type Definition and Typing Rules of
λ
FGThe type definition inλFGis given as follows:
σσ→σ|σ+σ|σ×σ{function, coproduct, product types}
| List(σ)|Bool {list and boolean types}
| Label|GXY {label and graph types}
The typing rules for graph-related expressions inλFGare given as follows:
(a∈ L)
⊢a:Label
⊢e1 :Label ⊢e2 :Label
⊢e1 =e2:Bool
⊢[] :GY
⊢e1:GXY⊢e2:G
X Y
⊢e1e2:GXY
⊢e1:Label ⊢e2:GY
⊢[e1:e2] :GY
(&y∈Y)
⊢[&y] :GY
⊢e:GY
⊢&x≔e:GY{&x} ⊢() :G∅Y
⊢e1:GXY1 ⊢e2:G
X2
Y (X1∩X2=∅)
⊢e1⊕e2:GXY1∪X2
⊢e1:GXY ⊢e2:G
Y Z
⊢e1@e2:GXZ
⊢e:GX
X∪Y(X∩Y=∅)
⊢cycle(e) :GX Y
⊢e:GX
Y
⊢isEmpty(e) :Bool
⊢e:Label×GY→GZZ ⊢d:List(GZZ×α+GZZ×Y)→GZZ×α+Z×Y
⊢srec(e,d) :GX
Y→G Z×X Z×Y
We have omitted the rules for lambda terms, which are standard. Note that for rules likee1e2, we do not require the output markers ofe1ande2to be identical. Here, we just choose a setY, which is a superset of the set of output markers of both expressions. Moreover, for rules like [], there is exactly the default marker&in the setX, which is why it is not mentioned.
C
Formal Semantics of Traceable Forward Evaluation
In this section we present the complete semantics of traceable forward evaluation that generates traceable views, in a similar way to the semantics ofUnCALO[12]. The for-ward semanticsF[[ep]]ρfor aλ
FG expressioneand a variable binding environmentρ
is inductively defined on the structure ofe. We complete the semantics for λFG here
together with the contents in Section 4.
Graph Constructors Expressions
The enriched forward semantics of the expressione1e2is defined as below. Note thatretains the order of the new branches when they link the input nodes.
F[[(e1e2)p]]ρ=F[[e1]]ρpF[[e2]]ρ
where G1pG2 =(V1∪V2∪V′,B1∪B2∪B′,I′) (V1,B1,I1)=G1,(V2,B2,I2)=G2
M =inMarker(G1)=inMarker(G2)
V′={Code p&m|&m∈M}
B′={Code p&m→[Edge(ǫ,I1(&m)),Edge(ǫ,I2(&m))]|&m∈M}
I′={&m→Code p&m|&m∈M}
where p is a union operator for two graphs concerning position p. We write
inMarker(G) andoutMarker(G) to denote the set of input and output markers in a graphG, respectively.
e1⊕e2is a componentwise union operator like, except that noǫ-edges are involved
to concatenate two subgraphs.
F[[(e1⊕e2)p]]ρ=F[[e1]]ρ⊕F[[e2]]ρ
whereG1⊕G2=(V1∪V2,B1∪B2,I1∪I2) (V1,B1,I1)=G1; (V2,B2,I2)=G2
The forward semantics for theempty graph constructor and theconstant marker
graphare defined as follows.
F[[()p]]ρ =({},{},{})
F[[[&m]p]]ρ=({
Code p},{Code p→[Outm(&m)]},{&→Code p})
The next two constructorsprepend labeled edges and markerswith a graph
respec-tively.
F[[[l:e]p]]ρ=({Code p} ∪V,{Code p→[Edge(lρ,I(&))]} ∪B,{&→Code p}) where (V,B,I)=F[[e]]ρ
F[[(&m≔e)p]]ρ=(&m≔F[[e]]ρ)
where (&m≔G)=(V,B,I′)
(V,B,I) =G
I′ ={&m.&x→v|(&x→v)∈I}
Here “.” is the Skolem function introduced before.
e1@e2 appends two graphs by connecting the output marker branches of the left
operand and corresponding input nodes of the right operand withǫ-edges.
F[[(e1@e2)p]]ρ=F[[e1]]ρ @pF[[e2]]ρ where G1@pG2=(V1∪V2,B′1∪B2,I1)
(V1,B1,I1)=G1,(V2,B2,I2)=G2
B′
1={u→
x.i=Edge(l,v) ⇒ x.i
=Outm(&m)⇒Edge(ǫ,I2(&m))
i∈|x|
|(u→x)∈B1}
